
\newcommand{\ccsrp}{\ensuremath{CCS_{rec}^p}}

\newcommand{\nset}[1]{\ensuremath{Nodes}(#1)}

\newcommand{\Tree}{\mathtt{Tree}}
\newcommand{\Comp}{\mathtt{Comp}}
\newcommand{\Pass}{\mathtt{Pass}}
\newcommand{\ClSub}{\mathtt{ClSub}}



\paragraph{Language}

CCS + recursion no restriction plus passivation

\begin{figure}[t]



 \caption{{LTS for \ccsrp.
Rules \textsc{Act2} and \textsc{Tau2}, the symmetric counterparts of 
\textsc{Act1} and \textsc{Tau1}, have been omitted.
} \label{fig:ltsccs}}
\end{figure}






\begin{myfact}\label{f:fbccs}
The LTS for \ccsrp given in Figure \ref{fig:ltsccs} is finitely branching.
\end{myfact}

% \paragraph{Kruskal Theory}
% 
% TO DO
% 
% 1) definizione di $\preceq^{tr}$

\paragraph{Termination is decidable in \ccsrp}

In contrast to the case of \ccsb, in order to prove that termination is decidable in \ccsrp we need to appeal to the theory of Kruskal on wqo on trees. 
This is due to the presence of recursion which generates processes of unbounded depth. (Esempietto?) 
Nevertheless some regularity can be found also in this case. By mapping processes into particular forms of trees and then exploitng an ordering between those trees it can be proven that this is indeed a well quasi ordering with strong compatibility, thus proving that termination is decidable.

In order to show the existence of a well structured transition system for \ccsrp we need to introduce some terminology.

% \begin{definition}[Normal form]
% forma normale 
% 
% $P \equiv \prod_{i=1}^{n} P_i \parallel \prod_{j=1}^{m} \pass{a_j}{P'_j} $
%  
% \end{definition}


\begin{lemma}\label{lem:normalform}
 Every process $P \in \ccsrp$ is equivalent to a process in normal form
$P \equiv \prod_{i=1}^{l} P_i \parallel \prod_{j=1}^{m}\prod_{k=1}^{n_j} \pass{a_j}{P'_{j,k}} $

Nota: con lo stesso nome di pass ci possono essere piu' pass unit -> doppia produttoria

\end{lemma}


Let $P \in \ccsrp$, for Lemma \ref{lem:normalform} $P \equiv \prod_{i=1}^{l} P_i \parallel \prod_{j=1}^{m}\prod_{k=1}^{n_j} \pass{a_j}{P'_{j,k}} $
we denote with 
\begin{itemize}
 \item $\Comp(P) = \{ P_1, \dots, P_l  \}$ the set of parallel components present in $P$ different from a passivation unit: 
 \item $\Pass(P)$ the names of passivation units appearing in $P$
 \item $\subp(P) $ is defined inductively in the following way
 \[
\begin{array}{l}
\subp(a.P) = \{a.P\}\cup \subp(P) 
\\
\subp(\outC{a}) = \{\outC{a} \} \\
\subp(P \parallel Q) = \subp(P)\cup\subp(Q) \\
\subp(\pass{a}{P}) = \{ \til{a} \} \cup  \subp(P) \\
\subp(rec X.P) = \{rec X.P\} \cup \subp(P)
\end{array}
\]
 \item DA SISTEMARE $\ClSub(P) = \{ Q\sub{X}{rec X .R} \mid  , Q \in \subp(rec X . R) \subseteq \subp(P) \text{ and $X$ free in } Q \}$
il problema sta nel dire che rec X.R e' esattamente il processo da sostituire alla X libera di Q come in papero gigio
 \item $\nset{P} = \subp(P) \cup \ClSub(P)$. $\nset{P}$ contains all the subterms appearing in $P$, the passivation names and the closure of subterms in $P$ (SPECIFICARE MEGLIO)

\end{itemize}

e.g. $P = \pass{a}{P_1} \parallel a.P_2$, $\Comp(P)=\{a.P_2\}$

1) definire albero di un processo e sua estensione a insieme di processi

\begin{definition}[Tree of a process]
 Let $P \in \ccsrp$ such that  $P \equiv \prod_{i=1}^{l} P_i \parallel \prod_{j=1}^{m}\prod_{k=1}^{n_j} \pass{a_j}{P'_{j,k}}$. The tree representation of $P$ denoted with $\Tree(P)$ is built as follows:
\begin{itemize}
 \item the labels of the nodes of $\Tree(P)$ are sequences of elements in $\nset{P}$
 \item the root is the sequence of all  the elements in $\Comp(P)$
 \item the root has as many subtrees as the passivation units present in $P$,   the roots of these subtrees are labeled with the name of the passivation units: $n_1$ nodes labeled $\til{a}_1$, $n_2$ nodes labeled $\til{a}_2$ \dots, and their children are the recursive application of the function $\Tree$ to the processes $P'_{j,k}$
\end{itemize}
\end{definition}

With a little abuse of notation we extend in the expected way the previous definition to deal with sets of processes.

\begin{example}
 Disegnare esempio di albero
\end{example}


\begin{definition}[$\preceq$]
Let $P, Q \in \ccsrp$. $P \preceq Q$ iff there exists a function $f$ that maps nodes of $\Tree(P)$ in nodes of $\Tree(Q)$ such that
\begin{itemize}
 \item if $n$ is a node in $\Tree(P)$ its label is related to the one of the corresponding node $f(n)$ in $\Tree(Q)$ with the following relation  $n =^* f(n)$: l'etichetta del nodo $n$ in $P$ e' ``contenuta'' in quella del nodo corrispondete in $Q$
 \item if $m$ is an ancestor of $n$ then $f(m)$ is an ancestor of $f(n)$
 \item if $p$ is the minimal common ancestor of $m$ and $n$ with $p,m,n \in \Tree(P)$ then $f(p)$ is the minimal common ancestor of $f(m)$ and $f(n)$ in $\Tree(Q)$.
\end{itemize}
\end{definition}

3) dimostrare che  preceq equivale a $ =^{tr}$
%Controllare se e' veramente necessario il requisito su nset, direi di no 
\begin{lemma}\label{lem:equivpreceq}
 Let $P,Q \in \ccsrp$.  %$\nset{P} = \nset{Q}$ and 
$P \preceq Q$ iff  $\Tree(P) =^{tr} \Tree(Q)$.
\end{lemma}
\begin{proof}
  Obvious from the definition of $\preceq$ and $=^{tr}$.
\qed
\end{proof}

4) definire l'insieme di tutti gli alberi generati a partire da nset{P}

\begin{definition}
 Let $P \in \ccsrp$. ${\cal T}_P$ is the set of all trees whose labels of nodes are sequences of elements in $\nset{P}$.
\end{definition}

5) dimostrazione di WQO

\begin{theorem}[Well-quasi-order]\label{th:wqoccs}
 Let $P \in \ccsrp$. The relation $=^{tr}$ is a well-quasi-order over ${\cal T}_P$.
\end{theorem}
\begin{proof}

The set $\nset{P}$ is finite by construction. By Proposition \ref{prop:eqwqo} the equality is a wqo over $\nset{P}$.
By Lemma \ref{lem:Higman}, and since $=$ is a wqo on $\nset{P}$,  $=^*$ is a wqo over $\nset{P}^*$.
Finally, by Lemma \ref{lem:Kruskal} and since $=^*$ is a wqo, $=^{tr}$ is a wqo over ${\cal T}_P$.
\qed
\end{proof}

6) devo dimostrare che deriv(P) subseteq tree(P), ho bisogno di un lemma ausiliaro


\begin{lemma}\label{lem:propnodes}
Let $P \in \ccsrp$. 
\begin{enumerate} 
 \item If $P \equiv P_1 \parallel P_2$ then $\nset{P}=\nset{P_1} \cup \nset{P_2}$.
 \item If $P \equiv \pass{a}{P_1}$ then $\nset{P}= \{\til{a}\} \cup \nset{P_1}$.
 
\end{enumerate}

\end{lemma}
\begin{proof}
 Straightforward from the definition of $\nset{P}$.\qed
\end{proof}




\begin{lemma}\label{lem:contenuto}
 Let $P \in \ccsrp$. If $P \pired Q$ then $\nset{Q} \subseteq \nset{P}$.
\end{lemma}
\begin{proof}
By case analysis on the rule used to infer reduction $P \pired Q'$.

We content ourselves with illustrating the case when the reduction is a syncrhonization between an input process inside a recursive process and a passivation unit, i.e. $P \equiv rec X. a.P_1 \parallel \pass{a}{P_2} \parallel P_3 $.
The othere ones are similar or simpler.

From the definition of $\nset{}$ and from Lemma \ref{lem:propnodes} we know that $\nset{P} = \{ rec X.a.P_1\} \cup \subp{P_1} \cup \ClSub(rec X. a.P_1) \cup \{\til{a}\} \cup \nset{P_2} \cup \nset{P_3}$.
If $P \pired Q$ then $Q \equiv P_1\sub{X}{rec X.a.P_1} \parallel P_3 $ and $\nset{Q} = \subp{P_1\sub{X}{rec X.a.P_1}} \cup \ClSub(P_1\sub{X}{rec X.a.P_1})  \cup \nset{P_3}$.

It is easy to see that $ \subp{P_1\sub{X}{rec X.a.P_1}} \cup \ClSub(P_1\sub{X}{rec X.a.P_1}) \subseteq \ClSub(rec X. a.P_1)$. This follows from the definition of $\ClSub(P)$ and by observing that all the processes in $\subp{P_1\sub{X}{rec X.a.P_1}}$ are processes of $\subp{P_1}$ where the free occurrences of $X$ have been replaced with $rec X.a.P_1$ hence processes in $\ClSub(rec X. a.P_1)$. A similar reasoning can be conducted for processes in $\ClSub(P_1\sub{X}{rec X.a.P_1})$.


\qed
\end{proof}

\begin{remark}
 Notice that if $P \pired Q$, $\nset{P} \subseteq \nset{Q}$ as stated in the previous Lemma \ref{lem:contenuto} but $\Tree(P) \neq ^{tr} \Tree(Q)$ since some labels can be consumed and some subtrees could have been disappeared for instance when it occurs a synchronization between an input and a passivation unit.
\end{remark}


\begin{corollary}\label{cor:derivccs}
 Let $P \in \ccsrp$. Then $\Tree(\deriv{P}) \subseteq {\cal T}_P$.
\end{corollary}
\begin{proof}
 The proof follows easily from Lemma \ref{lem:contenuto}. \qed
\end{proof}




The last thing to show is that the well-quasi-ordering $\preceq$ is strongly compatible 
with respect to the LTS in Figure \ref{fig:ltsccs}.


\begin{theorem}[Strong Compatibility]\label{th:scccs}
Let $P,Q,P' \in \ccsrp$. If $P \preceq Q$ and $P \pired P'$ then there exists $Q'$ such that $Q \pired Q'$ and $P' \preceq Q'$. 
\end{theorem}
\begin{proof}
By case analysis on the rule used to infer reduction $P \pired P'$. 
We content ourselves with illustrating the case when the reduction is a syncrhonization between an input process inside a recursive process and a passivation unit, i.e. $P \equiv rec X. a.P_1 \parallel \pass{a}{P_2} \parallel P_3$.
The othere ones are similar or simpler.

We first consider the modifications to $\Tree(P)$ when $P \pired P'$. The new $\Tree(P')$ is obtained from $\Tree(P)$ in the following way:
\begin{itemize}
 \item the subtree with root $\til{a}$ is removed.
 \item the label $rec X. a.P_1$ contained in the root is removed.
 \item the tree $\Tree(P_1)$ is \emph{added} in such a way that the labels contained in the root of $\Tree(P_1)$ are added to the ones in root of $\Tree(P)$, all the children of the root of $\Tree(P_1)$ are added to the root of $\Tree(P)$.
\end{itemize}

Now from Lemma \ref{lem:equivpreceq} we know that, since $P \preceq Q$, $\Tree(P) =^{tr} \Tree(Q)$. Hence there exists a mapping $f$ that associates nodes in $\Tree(P)$ to nodes in $\Tree(Q)$ such that there is a node $m$ in $\Tree(Q)$ whose label contains $rec X. a.P_1$. Similarly there exists a children of this node labeled with $\til{a}$.
So the same synchronization of before can take place in $Q$: $Q \pired Q'$.
Now $\Tree(Q')$ is obtained from $\Tree(Q)$ by applying the same modification as before to node $m$ instead of the root.

The last thing to show is that $P' \preceq Q'$, this follows easily by observing that the mapping between $\Tree(P')$ and $\Tree(Q')$ is the same $f$  pf the mapping between $\Tree(P)$ and $\Tree(Q)$ for all the nodes that has not been modified by the reduction. and there is a correspondence one to one for the other nodes.
\qed 
\end{proof}


\begin{theorem}\label{th:wstsccs}
 Let $P$ be a \ccsrp process. 
The transition system $(\deriv{P}, \pired, \preceq)$ is a finitely branching well-structured transition system with strong compatibility, decidable $\preceq$, and computable $Succ$.
\end{theorem}
\begin{proof}
 The transition system of \ccsrp is finitely branching (Fact \ref{f:fbccs}). The fact that $\preceq$ is a well-quasi-order on $\deriv{P}$ follows from Lemma \ref{lem:equivpreceq}, Theorem \ref{th:wqoccs} and Corollary \ref{cor:derivccs}. Strong compatibility follows from Theorem \ref{th:scccs}.
\qed \end{proof}

We can now state the main technical result of the section. 

\begin{corollary}
Let $P \in \ccsrp$ be a closed process. Then, termination of $P$ is decidable.
\end{corollary}
\begin{proof}
This follows from Theorems \ref{th:Finkel} and \ref{th:wstsccs}.
\qed \end{proof}